p:FinProbSpace, P, Q:((Outcome)).
(s:(Outcome). Q(s)  P(s))  nullset(p;P)  nullset(p;Q) 

latex

Definitions	x(s), t  T, P  Q, x:A. B(x), x:AB(x), f(a), s  C, Outcome, , Type, x:A  B(x), P & Q, measure(C)  q, , A c B, x:A. B(x), , #$n, r < s, , {x:A| B(x)} , p-open(p), nullset(p;S), FinProbSpace
Lemmas	nullset wf, finite-prob-space wf, rationals wf, qless wf, int inc rationals, p-open-member wf, p-measure-le wf, nat wf, p-outcome wf